\documentclass[envcountsame,english]{llncs}
\usepackage{babel,url,color}
\usepackage{latexsym,amssymb,amsmath,ifthen,alltt,array,enumerate}
\usepackage{tikz}
\usepackage{float}

\newcommand{\m}[1]{\mathsf{#1}}
\newcommand{\mi}[1]{\mathit{#1}}
\newcommand{\GG}{\mathcal{G}}
\newcommand{\seq}[2][n]{{#2_1},\dots,{#2_{#1}}}

\def\test#1#2#3{\setbox0=\hbox{$\vphantom{#1}^{#2}_{#3}$}%
                \dimen0=\wd0%
                \setbox1=\hbox{$\scriptstyle #2$}%
                \advance\dimen0-\wd1%
                \setbox1=\hbox{\hskip\dimen0\copy1}%
                \dimen0=\wd0%
                \setbox2=\hbox{$\scriptstyle #3$}%
                \advance\dimen0-\wd2%
                \setbox2=\hbox{\hskip\dimen0\copy2}%
                {\vphantom{#1}^{\box1}_{\box2}}{#1}
}


\newcommand{\SAT}{3-SAT }
\newcommand{\NP}{NP}
\newcommand{\PSPACE}{PSPACE}
\newcommand{\QBF}{\texttt{QBF }}
\newcommand{\tod}{\overset{d}{\to}}
\newcommand{\toa}{\overset{a}{\to}}

% for editing
\newcommand{\comment}[1]{\begin{center}\color{red}\tt #1 \end{center}}
\newcommand{\FB}[1]{{\color{red}#1}}
\newcommand{\DK}[1]{{\color{blue}#1}}

\newcommand{\dd}{{\langle d \rangle}}

\tikzstyle{mystyle}=[semithick]
\tikzstyle{ledge}=[font=\scriptsize]
\tikzstyle{final}=[circle,draw,minimum size=0.1cm,inner sep=1.7pt]

\begin{document}

\bibliographystyle{lncs}
\pagestyle{plain}


\title{The Multi-Agent Sabotage Game}

\mainmatter

\author{Fran\c{c}ois Bonnet \and Xavier D\'efago \and Dominik Klein}

\institute{School of Information Science\\
Japan Advanced Institute of Science and Technology\\
  Nomi, Japan}

\maketitle

\begin{abstract}
We consider an abstract scenario of malicious agents invading a network, 
modeled as a game. The globally-controlled agents move 
alternatively with a defender: in each turn, 
each agent moves alongside an edge on a directed acyclic graph (DAG), 
trying to reach a single, designated goal vertex, after which 
the defender is allowed 
to remove one edge from the DAG. We show that the 
problem of deciding whether there exists a strategy for the defender to 
disconnect the goal before one of the agents reaches it, is PSPACE-complete 
in general, and that it shifts to NP-complete if we assume an infinite supply
of agents. Moreover, we show that if we fix a constant number of agents and
consider only trees, the problem can be decided in 
polynomial time in the size of the tree.
Our work extends results on the Sabotage Game and the Firefighter-problem,
introduced respectively in 2001 by van Benthem and in 1995 
by Hartnell.
\end{abstract}

\section{Introduction}
Measuring the reliability of a network under faults is an important task in several
domains, 
especially in the context of analyzing reactive systems.
A natural modeling of such scenarios is the use of two-player games, where one 
player tries to establish a connection between nodes, whereas the other player
tries to destroy this connection. Very famous is the 
%XD: Add a footnote to explain shannon-switching game.
Shannon-Switching Game\footnote{In the Shannon-Switching Game, one
player tries to connect two given vertices of a graph by coloring edges,
while the second player tries to disconnect these vertices by removing edges.}~\cite{LEH64},
but a large number of other graph based games exist~\cite{DEM01}.
Recently, the ability of restoring destroyed links~\cite{RT07}, and 
other, more general reachability objectives, have been considered~\cite{GRT10}.

In 2001, van Benthem proposed the Sabotage Game~\cite{Ben05}, where 
the first player is subject to local movements in the graph, whereas the
other player is allowed to destroy links anywhere in the graph. 
More specifically, in this game played on graphs with
multi-edges, an agent (a ``Runner'' in their terminology) 
starts at a vertex trying to reach a designated goal, and
in each turn, the agent selects an outgoing edge from his current position 
and moves along that edge. The defender (the ``Blocker'') is then allowed 
to select one edge arbitrarily in the graph and reduce its 
multiplicity by one. The agent wins
if she has a strategy to reach the goal, despite any possible deletions by 
the defender, and she looses otherwise. Adding such dynamics makes
the analysis much more difficult, and often shifts the complexity to 
non-tractable complexity classes; one most notable exception being the 
Shannon-Switching Game. For
Sabotage Games, L\"oding and Rohde~\cite{LR03b} showed that the introduction of 
multi-edges shifts the problem to PSPACE-complete, whereas the game played
over a single-edge graph is decidable in linear time.

Our contribution extends their complexity result. We consider the case 
where the underlying
structure is quite restricted --- a cycle-free digraph ---, but
allow more than one agent to move through the graph.
In each turn, each of the agents, for which we assume some global control,
moves alongside an outgoing edge from its current position. Then the
defender is allowed to remove one edge from the graph and the next turn starts.
The agents win, if,
after several turns, at least one of them reaches the designated goal. We show that 
adding this kind of distributivity leads to a similar shift in complexity, 
even though the underlying, dynamically
changing structure is simpler. More specifically, our contribution includes 
the following four results:

%XD: Itemize -> enumerate
\begin{enumerate}
\item deciding whether the defender can always prevent 
$n$ agents from reaching the goal is PSPACE-complete, except for $n=1$.
\item playing against infinitely many agents shifts the problem
to NP-complete.
\item for games over trees and a fixed number of agents, we give an 
attractor-construction that computes whether the agents can be 
prevented from reaching the goal in time polynomial in the size of the tree.
\item games over trees however remain NP-hard for infinitely
many agents.
\end{enumerate}

To establish the last, we use 
a very straightforward reduction from \textsc{3-fl-fire}~\cite{KG10}, 
a variant of the Firefighter-problem on trees with reachability
conditions. 
%XD: rephrase slightly the following.
In the Firefigher-problem~\cite{H95}, a fire starts at a desginated vertex. In each step,
the Firefighter chooses a non-burning vertex to protect, which 
remains protected afterwards. Then, the fire spreads to all
adjacent vertices and continues, until it cannot spread anymore. The
Firefigher-problem requires to maximize the number of saved vertices.

The fourth result of course subsumes the second, since we regard 
a tree as a special kind of DAG.
We would like to stress however that, establishing NP-hardness 
of \textsc{3-fl-fire} itself is quite involved, reusing a central 
result from~\cite{FKMR07}
and several layers of reductions, whereas our proof of NP-hardness 
for playing against infinitely-many agents 
on DAGs is a direct reduction 
from \textsc{sat}, based on the completely different machinery 
we develop to establish the result of PSPACE-hardness, 
albeit requiring full DAGs.
%%%%%%%% XD: He did not understand the previous sentence. Could we remove "albeits requiring..."

This paper is structured as follows. In Section~\ref{sec:definitions}, we 
define the multi-agent sabotage game and the decision problems \textsc{$n$-agent blocking} 
and \textsc{$\infty$-agent blocking} for which we state complexity results.
PSPACE-completeness of the first is established in Section~\ref{sec:PSPACE-completeness}, while
the NP-completeness of the latter appears only in Appendix~\ref{sec:app-infty}, due to page limitation.
In Section~\ref{sec:tree}, we 
consider games over trees, and show that \textsc{$n$-agent blocking} 
can then be computed in time polynomial in the size of the tree for a constant number
of agents, but \textsc{$\infty$-agent blocking} remains NP-hard.
Finally, we conclude our presentation in Section~\ref{sec:Conclusion} 
and mention potential future work.


\section{Multi-Agent Sabotage Game}
\label{sec:definitions}

A multi-agent game is played on a game arena 
$\GG=(G,s,f)$ where $G=(V,E_{\text{in}})$ is a directed acyclic graph (DAG)\footnote{
All results presented here hold for unrestricted digraphs as well.},
$s$ is the \emph{initial} node, and $f$ is the \emph{goal} node.

%FB: I add some explanations.
For a game with $n$ agents on a graph $G=(V,E_{\text{in}})$, a \emph{configuration} is a 
tuple $(E,A)$, where $E$ is a subset of $E_{\text{in}}$, denoting the current set of edges
(i.e. $E$ does not contain the edges removed by the defender), and $A$ is a multiset 
of vertices $V$ with $|A|=n$, denoting the current positions of agents.
The game is played by alternating moves of the agents and the defender.
Let $(E,A)$ and $(E',A')$ be two configurations:
\begin{itemize}
\item A \emph{move of the agents} $(E,A) \toa (E',A')$ requires $E = E'$ 
and the existence of a multiset $S$ of vertices from $V$ and
a multiset $M$ of edges from $E$ such that
$A = S \uplus \{ s \mid (s,t) \in M \}$ and 
$A' = S \uplus \{ t \mid (s,t) \in M \}$, i.e., the agents in $S$ remain at
their position, whereas the others move alongside edges in $M$.
\item A \emph{move of the defender} $(E,A) \tod (E',A')$ requires
$A = A'$ and $E' = E \setminus \{e\}$ where $e \in E$, we say defender \emph{deletes} $e$.
\end{itemize} 

\noindent Let $\GG=(G,s,f)$ be a game arena with $G=(V,E_{\text{in}})$ and $|E_{\text{in}}|=k$.
Assuming $n$ agents, the \emph{initial configuration} of $\GG$ is $c_{\text{in}}=(E_{\text{in}},A_{\text{in}})$ where 
$A_{\text{in}} = \{ \overbrace{s, \ldots, s}^{\text{$n$ times}} \}$.
For a configuration $c=(E,A)$, property $\text{win}(c)$ holds if
$f \not \in A$, i.e. no agent has reached the goal node.
The defender \emph{wins} in $\GG$ against $n$ agents, if 
\[
\forall c_1 \exists c'_1 \forall \ldots \forall c_{k-1} \exists c'_{k-1} \forall c_{k}\,\
c_{\text{in}} \toa c_1 \tod \ldots \toa c_{k-1} \tod c'_{k-1} \toa c_k \Rightarrow \text{win}(c_k)
\]
\noindent where $c_{\text{in}}$ denotes the initial configuration of $\GG$,
and $c_i$, $c_i'$ denote, respectively, configurations after a move of the agents and a move of the defender.
%DK I put definitions of decision problems back into this sectoin
%DK otherwise definition of A_in for inf. many runners is seperated from def. of dec. problem
We define the following decision problem:
\begin{description}
\item
\textsc{$n$-agent blocking}:\\
\textsf{Input:} A game arena $\GG$. \\
\textsf{Question:} Does the defender win in $\GG$ against $n$ agents?
\end{description}

We also consider games against \emph{infinitely} many agents. The only difference
to games against finitely many agents is the initial configuration:  $c_{\text{in}}=(E_{\text{in}},A_{\text{in}})$ where $A_{\text{in}}$ is a multiset
containing node $s$ with multiplicity $\mathbb{N}$. The decision problem is:

\begin{description}
\item
\textsc{$\infty$-agent blocking}:\\
\textsf{Input:} A game arena $\GG$. \\
\textsf{Question:} Does the defender win in $\GG$ against infinitely many agents?
\end{description}



\section{Complexity results}\label{sec:PSPACE-completeness}

\begin{theorem}\label{thm:all-results}
The complexity of the \textsc{agent blocking} problems depends on the number of agents, namely:
\begin{enumerate}
\item[a.] \textsc{$1$-agent blocking} is decidable in linear time~\cite{LR03b}.
%\footnote{This problem can be even solved in constant time, depending on the encoding of the game arena.} time~\cite{LR03b}.%FB: Could remove the footnote if you do not like it.
%DK removed the footnote again. I tried to construct a turing-machine that runs in constant time, but ... I am not sure, if it is possible.
\item[b.] \textsc{$n$-agent blocking} is PSPACE-complete for all $n \geq 2$.
\item[c.] \textsc{$\infty$-agent blocking} is NP-complete.
\end{enumerate}
\end{theorem}

Theorem~\ref{thm:all-results}.a corresponds to a special case of the Sabotage Game, where the multiplicity of each edge is limited to one: The agent wins if and only if $s=f$ or $(s,f)\in E_{\text{in}}$. If not, the defender has the following winning strategy: When the agent is located at vertex $v$ and there is an edge $(v,f) \in E$, then delete $(v,f)$ otherwise delete an edge arbitrarily.

Proving Theorem~\ref{thm:all-results}.b is the subject of Section~\ref{sec:PSPACE-completeness}, and Theorem~\ref{thm:all-results}.c is a consequence of Theorem~\ref{thm:tree_np}. A direct proof for Theorem~\ref{thm:all-results}.c, based on methods developed to prove Theorem~\ref{thm:all-results}, is provided in the Appendix~\ref{sec:app-infty}, due to space reasons.
%XD: Some modifs to names of theorems.


%XD: I do not know how to put small capital in the name of subsection
\subsection{PSPACE-completeness of \textsc{$n$-agent blocking}}
To prove Theorem~\ref{thm:all-results}.2, we need to show 
membership in PSPACE, 
and PSPACE-hardness. The former can be shown by a 
depth-first game-tree construction, here we focus 
only on the latter. For it, we give a reduction from 
the PSPACE-complete problem of Quantified Boolean 
Formula (\textsc{qbf})~\cite{ST73}. 


Let
$\psi = \forall X_1 \exists X_2 \ldots Q X_{m-1} Q X_m \varphi$
be an instance of \textsc{qbf}, where $Q$ is $\forall$ for $m$ odd and $\exists$ for $m$ even,
and $\varphi$ is a quantifier-free formula 
over the $m$ Boolean variables $X_1, \ldots X_m$ in conjunctive normal form
with $p$ clauses.
Note that, w.l.o.g., we can assume that each clause contains 
exactly three distinct literals. 
Unless stated otherwise, we use indexes in the following 
way: $1 \leq i \leq m$ ranges
over the $m$ variables, $1 \leq j \leq p$ over clauses and
$1 \leq k \leq 3$ over literals of clauses. Thus $L_{jk}$ denotes
the $k$-th literal of the $j$-th clause:
$$\varphi = (L_{11}\vee L_{12}\vee L_{13})\wedge\ldots\wedge (L_{j1}\vee L_{j2}\vee L_{j3})\wedge\ldots\wedge (L_{p1}\vee L_{p2}\vee L_{p3})
$$


For a given $\psi$ and a given $n$,
we will construct a (parametrized) game arena 
$\GG^{n}_{\psi}$ with $n$ agents placed at the starting node.


\begin{lemma}\label{lem:g_qbf_psi}
Let $\psi$ be an instance of \textsc{qbf} and 
$n \geq 2$. The defender wins on $\GG^{n}_{\psi}$ 
iff $\psi$ has a satisfying assignment.
\end{lemma}

Lemma~\ref{lem:g_qbf_psi} and polynomial size of the game arena
in the size of $\psi$ and $n$, proves  the second case of Theorem~\ref{thm:all-results}.
The rest of this section 
shows how to construct $\GG^{n}_{\psi}$.
First note the two following simple facts: (i) As soon as the
agents reach a configuration $c$ where $\text{win}(c)$ holds,
the game is essentially over. Indeed the agents located at the goal
node just remain there until all edges have been deleted.
(ii) If there are $n$ agents and $n-1$ are
``stuck'', i.e. have no outgoing edge to move on, the last
agent can be stopped with the strategy described for the games
where there is only one agent. In the reduction we will make use of 
these facts and the interaction of precisely two agents 
that have to behave in a certain way in order
to prevent one agent from being stuck.

We adapt the idea used for the reduction of the
Sabotage Game~\cite{LR03b} to our setting. Naturally,
our construction is different since we are in 
a different setting,
but the following underlying principle is 
employed: we construct
a game arena, where first, the agents and the defender 
make an assignment of the variables \emph{in the graph} 
by their movements. 
If this assignment satisfies the formula, then the defender
wins in a later part of the graph, and she looses otherwise. In
particular we use the following substructures:


\begin{itemize}
 \item The \emph{filtering-gadget} is used as a barrier such that when $n$ agents enter it, precisely two agents are able to pass it.
 \item A \emph{universal-gadget} corresponds to a universally quantified variable. The 
 movements of the agents determine whether the corresponding variable is set 
 either to \textsc{true} or \textsc{false}.
\item An \emph{existential-gadget} corresponds to one existentially quantified variable. Depending on his deletions, the defender may assign \textsc{true} or \textsc{false} to the variable.
 \item The \emph{verification-gadget}: Here the agents can choose a clause --- with the intention of showing that the defender's assignment of variables is not a satisfying one ---, and after the movements lead to that clause, by subsequent deletions, the defender can choose one literal in the clause, with the intention of showing that for any clause there is at least one literal that satisfies it.
\end{itemize}


The gadgets will be connected in the following way: 
the start of the game arena $\GG^n_{\psi}$ is the filtering-gadget; the starting node 
$s$ of the game arena is the node $s_0$ of this gadget.
The exit node $s_1$ of the filtering gadget corresponds to the entry of the 
universal-gadget for $X_1$, whose exit node $s_2$ corresponds to the entry
of the existential-gadget for $X_2$ etc., until the last variable gadget for $X_m$,
whose exit node $s_{m+1}$ is connected to the verification-gadget.
We define the correspondence of an assignment of the variables of $\psi$ and 
movements and deletions in $\GG^n_{\psi}$. Here nodes $x_i$ and $\neg x_i$ denote two 
particular nodes of the graph:

\begin{definition}
Let $\GG^n_{\psi} = (G,s,f)$ be the game arena for a given instance $\psi$ of \textsc{qbf}, and $(E,A)$ a configuration. Variable
$X_i$ is assigned \emph{in} $\GG^n_{\psi}$ to
\begin{align*}
&\text{\textsc{false}, when $(x_i,f) \in E$ and $\textsf{outdeg}(\neg x_i) = 0$}  \\
&\text{\textsc{true}, when $(\neg x_i,f) \in E$ and $\textsf{outdeg}(x_i) = 0$}  
\end{align*}
We write $\GG^n_{\psi}(X_i) = \textsc{true}$ resp. $\GG^n_{\psi}(X_i) = \textsc{false}$,
and we write $\alpha(\GG^n_{\psi})$ to denote 
the assignment of the variables of $\psi$ where $X_i = \textsc{true}$ when 
$\GG^n_{\psi}(X_i) = \textsc{true}$ and $X_i = \textsc{false}$ when $\GG_{\psi}^n(X_i) = \textsc{false}$.
\end{definition}

%FB: I added some explanations in the following paragraph.
In the following figures we often draw multiple goal nodes (represented by $\odot$). This is only for the ease of illustration, and all goal nodes of all occurring gadgets can be actually merged into a single goal node. Note that in our construction, one node is never connected to multiple ``different'' goal nodes; thus the merging of all the goal nodes does not create multi-edges.

%I removed the *, I like when sections have numbers :p
\subsection{The filtering-gadget}

The initial state of the filtering-gadget for $n$ agents, before any edge-removal by the defender, is shown in Figure~\ref{fig:filtering-gadget_init}, and the agents are about to move. The filtering-gadget has the following property:

\begin{lemma}\label{lem:filtering}
Let $G$ be a graph containing a filtering gadget. The defender wins in $(G,s_0,f)$ against $n$ agents iff the defender wins in $(G,s_1,f)$ against two agents.
\end{lemma}

Assume one agent moves to each $a_{i,1}$ for $1 \leq i \leq n-2$. Moving more than one agent to one of the $a_{i,1}$ is not optimal, since from each $a_{i,1}$ there is only a single path to the goal. The remaining two agents move to $b_1$. The defender has to remove the edge $(a_{1,1},f)$, the agents proceed to $b_{2}$ and $a_{i,2}$ for $2 \leq i \leq n-2$, the defender removes the edge $(a_{2,2},f)$, and so on, until the agents reach $a_{n-2,n-2}$ and $b_{n-2}$. The defender removes the edge $(a_{n-2,n-2},f)$, and two agents reach $s_1$ from $b_{n-2}$. Any other movements of players lead to a loss for them.

\begin{figure}[t]%
  \centering 
 \parbox{0.45\textwidth}{%
  % The initial filtering gadget
  \begin{tikzpicture}[scale=0.5,node distance=1cm,style=mystyle]
    \tikzstyle{every to}=[->] %make all edges directed

    \node[]  								(a)		at (0,0)  {$s_0$};    
    
    \node[]									(a21)		[below of=a] 	{$a_{2,1}$};
	\node[]									(a11)		[left of=a21] 	{$a_{1,1}$};
	\node[]									(b1)		[left of=a11]	{$b_1$};
	
	\node[node distance=2cm]				(am1)		[right of=a21] 	{$a_{n-2,1}$};
    
    \node[]									(b2)		[below of=b1]	{$b_2$};
    \node[]									(a22)		[below of=a21]	{$a_{2,2}$};
    
    
    \node[node distance=2cm, style=final]	(f)	 		[below of=a22]	{$\bullet$}; 
    \node[node distance=3cm]				(bm)		[below of=b1]	{$b_{n-2}$};
    \node[]									(b)			[below of=bm]	{$s_1$};
    
    \node[node distance=3cm]				(amm)		[below of=am1]	{$a_{n-2,n-2}$};
    
 	\draw[style=dotted] (a21) 	to[-] node[auto] {} (am1);
	\draw[style=dotted] (b2) 	to[-] node[auto] {} (bm);
	\draw[style=dotted] (am1) 	to[-] node[auto] {} (amm);
	
	\draw[]						(a)		to node[auto]	{}	(b1);
	\draw[]						(b1)	to node[auto]	{}	(b2);
	\draw[]						(bm)	to node[auto]	{}	(b);	
	\draw[]						(a)		to node[auto]	{}	(a11);
	\draw[]						(a21)	to node[auto]	{}	(a22);				
	\draw[]						(a)		to node[auto]	{}	(a21);
	\draw[]						(a)		to node[auto]	{}	(am1);
	
	\draw[bend right = 20]		(a11)	to node[auto]	{}	(f);
	\draw[]						(a22)	to node[auto]	{}	(f);
 	\draw[bend left = 20]		(amm)	to node[auto]	{}	(f);
  
    
  \end{tikzpicture}
  \caption{The filtering-gadget}
  \label{fig:filtering-gadget_init}  } %
  \parbox{0.45\textwidth}{%
  % The universal gadget
  \begin{tikzpicture}[scale=0.5,node distance=1cm,style=mystyle]
   \tikzstyle{every to}=[->] %make all edges directed

 	\node[]								(a)		at (0,0)			{$s_i$};

	\node[]								(c1)		[below left of=a] 	{$c_1$};
	\node[]								(c2)		[below right of=a] 	{$c_2$};	
	\node[]								(d1)		[below left of=c1] 	{$d_1$};	
	\node[]								(d2)		[below right of=c2] {$d_2$};

	\node[node distance=2cm]			(e1)		[below left of=d1]	{$e_1$};
	\node[node distance=2cm]			(e2)		[below right of=d1]	{$e_2$};
	
	\node[]								(g1)		[right of=e1]		{$x_i$};
	\node[]								(g2)		[left of=e2]		{$\neg x_i$};

	\node[node distance=2cm]			(h1)		[below of = e2]		{$h_1$};
	\node[]								(i1)		[below of = h1]		{$i_1$};
    \node[style=final]					(f3) 		[right of=i1]		{$\bullet$}; 
	\node[]								(b)			[below of = f3]		{$s_{i+1}$};

    \node[node distance=2.4cm,style=final](f0) 		[right of=a]		{$\bullet$};
    \node[node distance=2.4cm,style=final](f1) 		[below of=d1]		{$\bullet$}; 
    \node[node distance=1.7cm,style=final](f2) 		[right of=c2]		{$\bullet$}; 
    \node[style=final]					(f3) 		[right of=d2]		{$\bullet$}; 
    \node[style=final]					(f4) 		[right of=i1]		{$\bullet$}; 

	\node[node distance=2cm]			(er)		[below right of=d2]	{$e_r$};
	\node[]								(hl)		[left of=er]		{$h_l$};
	\node[]								(hr)		[below of=er]		{$h_r$};
    \node[style=final]					(f5) 		[left of=hr]		{$\bullet$}; 
	\node[]								(i2)		[below of=f5]		{$i_2$}; 
	
	\node[node distance=1.4cm]			(from_veri1)[left of=d1]		{\tiny{ver. gadget}};
	\node[node distance=1.5cm]			(from_veri2)[below of=e1]		{\tiny{ver. gadget}};
 
	\draw[]								(a)			to node[auto]	{}	(c1); 		
	\draw[]								(a)			to node[auto]	{}	(c2); 		
	\draw[]								(c1)		to node[auto]	{}	(d1); 		
	\draw[]								(c2)		to node[auto]	{}	(d2); 			 	
	\draw[]								(d1)		to node[auto]	{}	(e1); 			 	
	\draw[]								(d1)		to node[auto]	{}	(e2); 			 	
	\draw[]								(e1)		to node[auto]	{}	(g1); 			 	
	\draw[]								(e2)		to node[auto]	{}	(g2); 			 	
	\draw[]								(g1)		to node[auto]	{}	(f1); 			 	
	\draw[]								(g2)		to node[auto]	{}	(f1); 			 	
	\draw[]								(e2)		to node[auto]	{}	(h1); 			 	
	\draw[bend left=-30]				(e1)		to node[auto]	{}	(h1); 			 	
	\draw[]								(h1)		to node[auto]	{}	(i1); 			 	
 	
	\draw[]								(i1)		to node[auto]	{}	(b); 			 	
	\draw[]								(i1)		to node[auto]	{}	(f4); 			 	

	\draw[]								(d2)		to node[auto]	{}	(er); 			 	
	\draw[]								(er)		to node[auto]	{}	(hl); 			 	
	\draw[]								(er)		to node[auto]	{}	(hr); 			 	
	\draw[]								(hl)		to node[auto]	{}	(f5); 			 	
	\draw[]								(hr)		to node[auto]	{}	(f5); 			 	
	\draw[]								(hr)		to node[auto]	{}	(i2); 			 	
	\draw[bend left=-40]				(hl)		to node[auto]	{}	(i2); 			 	
	\draw[bend right=-20]				(i2)		to node[auto]	{}	(b); 			 	
	\draw[]								(a)		to node[auto]	{}	(f0);
	\draw[]								(c2)		to node[auto]	{}	(f2); 			 	
	\draw[]								(d2)		to node[auto]	{}	(f3); 

	\draw[bend left=20,style=ledge,dotted]	(from_veri1) to node[auto] {} (g2);
	\draw[bend right=20,style=ledge,dotted]	(from_veri2) to node[auto] {} (g1); 	
 	
  \end{tikzpicture}
  \caption{The \emph{universal} gadget for $X_i$.}
  \label{fig:universal-gadget}
}

\end{figure}

\subsection{The universal-gadget}
A universal-gadget is shown in Figure~\ref{fig:universal-gadget}. 
One universal-gadget corresponds to one universally quantified variable. 
The universal-gadget corresponding to variable $X_i$ is connected
%FB: Added the brackets.
with the verification-gadget (described later) in the following way:
$(l_{jk},x_i) \in E_{\text{in}}$ iff $L_{jk} = X_i$, and 
$(l_{jk},\neg x_i) \in E_{\text{in}}$ iff $L_{jk} = \neg X_i$. Here
$l_{jk}$ is a node in the verification-gadget that correspond to the literal $L_{jk}$ of $\psi$.
In a universal-gadget, the agents may choose an assignment:

\begin{lemma}\label{lem:universal}
Let $X_i$ be the variable of a universal-gadget of $\GG^n_{\psi}$, and $(E,\{s_i, s_i\})$ be a configuration, where the edges of the gadget $E_u \subseteq E$ are intact. 
Let both player play optimally.
Then a traversal of the universal-gadget leads to a configuration $(E',\{s_{i+1}, s_{i+1}\})$ 
where $E' \setminus E_u = E \setminus E_u$ and, \emph{depending on the movements of the agents},  either 
$\GG^n_{\psi}(X_i) = \textsc{true}$ or $\GG^n_{\psi}(X_i) = \textsc{false}$.
\end{lemma}

Assume that two agents arrive at node $s_i$ (from either the filtering-gadget or a previous existential-gadget), then defender has to remove the edge $(s_i,f)$ otherwise he looses the game. For agents, moving both to $c_1$ leads to loss, as does moving both to $c_2$ after subsequent deletions of $(c_2,f)$, $(d_2,f)$, $(e_r,h_l)$, $(h_r,f)$, and $(i_2,b)$. Thus the agents split and move to $c_1$ and $c_2$, and after deleting $(c_2,f)$ arrive at $d_1$ and $d_2$, and $(d_2,f)$ is deleted. Now the left agent may decide to either move to $e_1$ (which will result in assigning $X_i$ to \textsc{false} in $\GG_{\psi}^n$) or to $e_2$ (which will result in  assigning $X_i$ to \textsc{true}), whereas the agent on $d_2$ moves to $e_r$. Assume the first. The defender has to delete either $(e_1,x_i)$ or $(x_i,f)$, otherwise he looses by moves of the agents to both $x_i$ and to either $h_l$ or $h_r$. The defender will remove $(x_i,f)$, as this blocks also all incoming edges from the verification gadget. After several subsequent moves and deletions, both agents arrive at $s_{i+1}$. The case when the left agent moves to $e_2$ is analogous, and
other movements of the players lead to their loss.

\begin{figure}[t]%
  \centering

  % The existential gadget
  \begin{tikzpicture}[scale=0.2,node distance=1cm,style=mystyle]
   \tikzstyle{every to}=[->] %make all edges directed

    \node[]								(b)	at (0,0)		{$s_i$};    
   
    \node[node distance=2.08cm, style=final](f) 	[below of=b]		{$\bullet$};    
    \node[node distance=1.5cm]			(bl)		[below left of=b]	{$b_l$};
    \node[node distance = 1.5cm]			(br)		[below right of=b]	{$b_r$};   

    \node[]								(cl)		[below of=bl]		{$c_l$};   
    \node[]								(cr)		[below of=br]		{$c_r$};   
    \node[]								(el)		[below of=cl]		{$x_i$};   
    \node[]								(er)		[below of=cr]		{$\neg x_i$};   
    \node[]								(dl)		[left of=el]		{$d_l$};   
    \node[]								(dr)		[right of=er]		{$d_r$};   
    \node[node distance=2cm]			(g)			[below of=f]		{$g$};
    \node[]								(o)			[below of=g]		{$s_{i+1}$};
    
    \node[node distance=2cm]			(h)			[left of=cl]		{$h$};    
    \node[]								(i)			[below of=h]		{$i$};
    \node[]								(j)			[left of=i]			{$j$};
    \node[]								(k)			[below of=i]		{$k$};
    \node[style=final]					(f2)		[below of=j]		{$\bullet$};

    \node[node distance=3cm]		(from_veri1)[above left of=i]	{\tiny{ver. gadget}};
    \node[node distance=1.5cm]		(from_veri2)[above right of=dr]	{\tiny{ver. gadget}};
 
	\draw[]							(b)		to node[auto]	{}	(bl); 
	\draw[]							(b)		to node[auto]	{}	(br);     
	\draw[]							(bl)	to node[auto]	{}	(cl); 	
	\draw[]							(br)	to node[auto]	{}	(cr); 		
	\draw[]							(cl)	to node[auto]	{}	(dl); 		
	\draw[]							(cr)	to node[auto]	{}	(dr); 		
	\draw[]							(dl)	to node[auto]	{}	(g); 	
	\draw[]							(dr)	to node[auto]	{}	(g); 	
	\draw[]							(dl)	to node[auto]	{}	(el); 	
	\draw[]							(dr)	to node[auto]	{}	(er); 	
	\draw[]							(g)		to node[auto]	{}	(o); 		
	
	\draw[]							(bl)	to node[auto]	{}	(h); 		
	\draw[]							(h)		to node[auto]	{}	(i); 	
	\draw[]							(i)		to node[auto]	{}	(k); 	
	\draw[]							(i)		to node[auto]	{}	(j); 	
	\draw[]							(k)		to node[auto]	{}	(o); 	
%	\draw[out=-130, in=-140,looseness=1.2]	(j)		to node[auto]	{}	(o); 			
	\draw[out=-130, in = -180]	(j)		to node[auto]	{}	(o); 			
	
	
	\draw[]							(cl)	to node[auto]	{}	(f); 	
	\draw[]							(bl)	to node[auto]	{}	(f); 	
	\draw[]							(cr)	to node[auto]	{}	(f); 	
	\draw[]							(br)	to node[auto]	{}	(f); 	
	\draw[]							(el)	to node[auto]	{}	(f); 	
	\draw[]							(er)	to node[auto]	{}	(f); 	
	\draw[]							(j)		to node[auto]	{}	(f2); 	
	\draw[]							(k)		to node[auto]	{}	(f2); 	

	\draw[bend left=30,style=ledge,dotted]	(from_veri1) to node[auto] {} (el);
	\draw[bend right=20,style=ledge,dotted]	(from_veri2) to node[auto] {} (er);
	\draw[looseness=2.5]		(br)	to node[auto]	{}	(h);	
  \end{tikzpicture}
  \caption{The initial \emph{existential} gadget for variable $X_i$.}
  \label{fig:existential-gadget}
\end{figure}

\subsection{The existential-gadget}
%DK put the subsec below def. of figure, otherwise
%bht places the figure directly under the subsection

An existential-gadget is shown in Figure~\ref{fig:existential-gadget}. 
One existential-gadget corresponds to one existantially quantified variable. 
The existential-gadget corresponding to variable $X_i$ is connected
with the verification-gadget in the following way:
$(l_{jk},x_i) \in E$ iff $L_{jk} = X_i$, and 
$(l_{jk},\neg x_i) \in E$ iff $L_{jk} = \neg X_i$, where
$l_{jk}$ is a node in the verification-gadget.
The key point here is that the defender can choose an assignment:

\begin{lemma}\label{lem:existential}
Let $X_i$ be the variable of an existential-gadget of $\GG^n_{\psi}$, and $(E,\{s_i, s_i\})$ be a configuration, where the edges of the gadget $E_e \subseteq E$ are the intact.
Let both player play optimally.
Then a traversal of the existential-gadget leads to a configuration $(E',\{s_{i+1}, s_{i+1}\})$ 
where $E' \setminus E_e = E \setminus E_e$ and, \emph{depending on the deletions of the defender}, either
$\GG^n_{\psi}(X_i) = \textsc{true}$ or $\GG^n_{\psi}(X_i) = \textsc{false}$.
\end{lemma}

Assume that two agents arrive at node $s_i$ (from a previous universal-gadget), 
the choice of the defender is done by deleting either $(s_i,b_l)$ or $(s_i,b_r)$ in the first step,
the former assigns $X_i$ to \textsc{true} in $\GG^n_{\psi}$, the latter to 
\textsc{false}. Consider the following traversals:
If neither $(s_i,b_l)$ or $(s_i,b_r)$ has been deleted, the 
agents win by moving one agent to $b_l$ and one to $b_r$ and 
then one of them to the goal, or, if either $(b_l,f)$ or 
$(b_r,f)$ has been deleted in the first step, 
by continuing to $(c_l,f)$ and $(c_r,f)$ and then moving 
one of the agents to the goal.

For now assume that the defender deletes $(s_i,b_r)$. 
Thus the agents move both to $b_l$, and defender removes 
$(b_l,f)$. Moving both agents to $h$ leads to loss by 
removing $(h,i)$, and moving both to $c_l$ also 
leads to loss by deleting $(c_l,f)$, then $(d_l,x_i)$ 
and finally $(g,s_{i+1})$. Thus the agents have to split 
and one moves to $h$ and one to $c_l$. Defender 
deletes $(c_l,f)$ and the agents move to $i$ and $d_l$.

If neither $(d_l,x_i)$ or $(x_i,f)$ is deleted, the 
agents win by moving both to $x_i$ and to either $j$ 
or $k$. It will be later seen that it is optimal now for the 
defender to remove the edge $(x_i,f)$, thereby disconnecting 
any link back from the verification gadget. Afterwards the 
agent at $d_l$ moves in two steps via $g$ to $s_{i+1}$, and 
the other one either via $k$ --- defender 
removing $(k,f)$ --- or via $j$ --- defender 
removing $(j,f)$ --- to $s_{i+1}$. 

    
  
\begin{figure}[]%
  \centering  
  % The verification gadget
  \begin{tikzpicture}[scale=0.3,node distance=1cm,style=mystyle]
   \tikzstyle{every to}=[->] %make all edges directed

 	\node[]								(a)			at (0,0) {$s_{m+1}$};
 	\node[node distance=0.8cm]			(fake2)		[below of=a]		{};
	\node[node distance=2cm]			(dl)		[left of=fake2]		{$d_l$};
	\node[node distance=2cm]			(dr)		[right of=fake2]	{$d_r$};
	\node[]								(el)		[below of=dl]		{$e_l$};
	\node[]								(er)		[below of=dr]		{$e_r$};
	\node[]								(fr)		[below of=er]		{$f_r$};
	\node[]								(fl)		[below of=el]		{$f_l$};
    \node[style=final, node distance = 3cm]			(f0) 		[right of=a]		{$\bullet$}; 
    \node[style=final]					(f1) 		[right of=dr]		{$\bullet$}; 
    \node[style=final]					(f2) 		[left of=el]		{$\bullet$}; 
    \node[style=final]					(f3) 		[right of=fr]		{$\bullet$}; 
    
    \node[]								(fake_c)	[below of=fl]		{$\cdots \cdots$};
    \node[]								(fake_c2)	[left of=fake_c]	{$l_{21}$};
    \node[]								(fake_ck)	[right of=fake_c]	{$l_{(p-1)1}$};
    \node[node distance = 1.5cm]		(c1)		[left of=fake_c	]	{$l_{11}$};    
    \node[node distance = 2cm]			(ck)		[right of=fake_c]	{$l_{p1}$};
    
    \node[]								(fake_right)[below of=fr]		{};    
    \node[]								(g)			[right of=fake_right]{$l_{r1}$};

	\node[]								(fake_mid1)	[below of = c1]		{};    
    \node[]								(fake_l11)	[left of=fake_mid1] {};
    \node[]								(h1)		[right of=fake_mid1]{$g_1$};
    
    \node[]								(fake_midk)	[below of=ck]		{};
    \node[]								(fake_lk1)	[left of=fake_midk]	{};
    \node[]								(hk)		[right of=fake_midk]{$g_p$};
    \node[]								(hl)		[below of=g]		{$g_l$};
    \node[]								(hr)		[right of=g]		{$g_r$};
    \node[style=final]					(f4) 		[right of=hl]		{$\bullet$}; 

	\node[]								(i1)		[below of=h1]		{$l_{12}$};
	\node[node distance=1.5cm]			(mid_dots)	[right of=i1]	{$\cdots \cdots$};
	\node[]								(ik)		[below of=hk]		{$l_{k2}$};
	\node[]								(i)			[below of=hl]		{$l_{r2}$};

	\node[]								(fake_mid2)	[below of=i1]		{};
	\node[]								(fake_l12)	[left of=fake_mid2]	{};
	\node[]								(j1)		[right of=fake_mid2]{$l_{13}$};

	\node[]								(fake_midk2)[below of=ik]		{};
	\node[]								(fake_lk2)	[left of=fake_midk2]{};
	\node[]								(jk)		[right of=fake_midk2]{$l_{k3}$};

	\node[]								(fake_mid3) [below of=j1]		{};
	\node[]								(fake_l13)	[left of=fake_mid3]	{};
	\node[]								(fake_midk3)[below of=jk]		{};
	\node[]								(fake_lk3)	[left of=fake_midk3]{};	
	
	\node[]								(jr)		[right of=i]		{$h_r$};
	\node[]								(jl)		[below of=i]		{$h_l$};
	\node[]								(jf)		[below of=jl]		{$l_{r3}$};
    \node[style=final]					(f5) 		[right of=jl]		{$\bullet$}; 

	\draw[]								(a)			to node[auto]	{}	(dl); 			 	
	\draw[]								(a)			to node[auto]	{}	(dr); 			 	
	\draw[]								(a)		to node[auto]	{}	(f0); 	 	
	\draw[]								(dl)		to node[auto]	{}	(el); 			 	
	\draw[]								(dr)		to node[auto]	{}	(er);
	\draw[]								(dr)		to node[auto]	{}	(f1); 	 			 	
	\draw[]								(er)		to node[auto]	{}	(fr); 			 	
	\draw[]								(el)		to node[auto]	{}	(fl); 	
	\draw[]								(el)		to node[auto]	{}	(f2); 				 	
	\draw[]								(fr)		to node[auto]	{}	(f3); 			 	
	\draw[]								(fl)		to node[auto]	{}	(c1); 				 	
	\draw[]								(fl)		to node[auto]	{}	(ck); 			 	
	\draw[]								(fr)		to node[auto]	{}	(g);	
	\draw[]								(g)			to node[auto]	{}	(hr);	
	\draw[]								(g)			to node[auto]	{}	(hl);
	\draw[]								(hr)		to node[auto]	{}	(f4);
	\draw[]								(hl)		to node[auto]	{}	(f4);
	\draw[]								(hl)		to node[auto]	{}	(i);
	\draw[]								(i)			to node[auto]	{}	(jr);
	\draw[]								(i)			to node[auto]	{}	(jl);	
	\draw[]								(jl)		to node[auto]	{}	(f5);
	\draw[]								(jr)		to node[auto]	{}	(f5);
	\draw[]								(jl)		to node[auto]	{}	(jf);
	\draw[]								(jf)		to node[auto]	{}	(f5);
	
	\draw[style=ledge,dotted]			(c1)		to node[auto]	{\tiny{back}}	(fake_l11);
	\draw[style=ledge,dotted]			(ck)		to node[auto]	{\tiny{back}}	(fake_lk1);
	\draw[]			(c1)		to node[auto]	{}	(h1);
	\draw[]			(ck)		to node[auto]	{}	(hk);	
	\draw[]			(h1)		to node[auto]	{}	(i1);	
	\draw[]			(hk)		to node[auto]	{}	(ik);	
	\draw[]			(i1)		to node[auto]	{}	(j1);	
	\draw[]			(ik)		to node[auto]	{}	(jk);	
	\draw[]			(fl)		to node[auto]	{}	(fake_c2);
	\draw[]			(fl)		to node[auto]	{}	(fake_ck);
	\draw[style=ledge,dotted]			(i1)		to node[auto]	{\tiny{back}}	(fake_l12);	
	\draw[style=ledge,dotted]			(ik)		to node[auto]	{\tiny{back}}	(fake_lk2);	
	\draw[style=ledge,dotted]			(j1)		to node[auto]	{\tiny{back}}	(fake_l13);	
	\draw[style=ledge,dotted]			(jk)		to node[auto]	{\tiny{back}}	(fake_lk3);	

	\draw[out=-5,in=20,looseness=1.1]		(hr)		to node[auto]	{}	(i);	
	\draw[out=-5,in=-10,looseness=1.1]		(jr)		to node[auto]	{}	(jf);	

	
  \end{tikzpicture}
  \caption{The verification-gadget with $p$ clauses.}
  \label{fig:verification-gadget}
\end{figure}

\subsection{The verification-gadget}

The verification gadget is depicted in Figure~\ref{fig:verification-gadget}. 
Here a node $l_{jk}$ corresponds to the literal $L_{jk}$ of $\psi$, and has outgoing links to the variable gadgets, as described.
There is a direct correspondence between winning conditions and assignments of literals:

\begin{lemma}\label{lem:veri_literals}
Let $\GG^n_{\psi}$ be the game arena of $\psi$, and $(E,A)$ a configuration,
where all variables of $\psi$ are assigned \emph{in} $\GG^n_{\psi}$, and
defender is about to move.
\begin{enumerate}
\item Let $A = \{ l_{j1}, l_{r1}\}$. Then defender wins if $\alpha(\GG^n_{\psi}) \models L_{j1}$.
\item Let $A = \{ l_{j2}, l_{r2}\}$. Then defender wins if $\alpha(\GG^n_{\psi}) \models L_{j2}$.
\item Let $A = \{ l_{j3}, h_{l}\}$ or $A = \{ l_{j3}, h_{r}\}$. Then defender wins iff $\alpha(\GG^n_{\psi}) \models L_{j3}$.
\end{enumerate}
\end{lemma}
\begin{proof}
W.l.o.g. let $L_{j1} = X_i$. For the first claim, since $\alpha(\GG^n_{\psi}) \models L_{j1}$, we have $\textsf{outdeg}(x_i) =0$, i.e. $x_i$ is a sink. Thus the defender wins by 
removing $(l_{j1},g_j)$ and applying the strategy described for one agent afterwards.
The second claim follows analogous. For the third claim, w.l.o.g. let $L_{j3} = X_i$. 
When $\alpha(\GG^n_{\psi}) \models L_{j3}$, the defender wins by removing
$(h_{l},f)$ (resp. $(h_{r},f)$) and $(l_{r3},f)$. 
When $\alpha(\GG^n_{\psi}) \not \models L_{j3}$,
after the deletion of the defender, the agents win by either moving 
from $h_l$ ($h_r$) to $f$ or by moving both to $x_i$ and $l_{r3}$, and 
then winning in the next step.
\end{proof}


Using Lemma~\ref{lem:veri_literals}, the following relation between
assignments in $\GG^n_{\psi}$ and winning conditions in the verification gadget
holds:

\begin{lemma}\label{lem:veri}
Let $\GG^n_{\psi}$ be the game arena of $\psi$, and let $(E,\{s_{m+1},s_{m+1}\})$
be a configuration, where all variables are assigned in $\GG^n_{\psi}$,
the edges of the verification gadget intact, and defender is about to move.
The defender wins iff $\alpha(\GG^n_{\psi}) \models \psi$.
\end{lemma}

A run through the verification gadget starts with two agents arriving at $s_{m+1}$ and
the defender removing $(s_{m+1},f)$. The agents need to split, as the defender wins by either removing $(d_l,e_l)$ or $(d_r,f)$ and then $(e_r,f_r)$. 
After two steps, the agents will reach $f_l$ and $f_r$, defender removing $(f_r,f)$.
The left agent can now choose a clause of the 
formula, with the intention to falsify it. Assume he decides 
to move to $l_{j1}$, whereas the right agent moves to $l_{r1}$. W.l.o.g. assume
$L_{j1} = X_1$, $L_{j2} = X_2$ and $L_{j3} = X_3$. 
If $\alpha(G^n_{\psi}) \models L_{j1}$, the defender wins by Lemma~\ref{lem:veri_literals}.1 and if $\alpha(G^n_{\psi}) \not \models L_{j1}$, he removes either $(x_i,f)$ or $(l_{j1},x_i)$.
The agents move to $g_1$ and $g_l$ ($g_r$), defender removes $(g_l,f)$ ($(g_r,f)$), agents move to $l_{j2}$ and $l_{r2}$. Now, if $\alpha(G^n_{\psi}) \models L_{j2}$, we can apply 
Lemma~\ref{lem:veri_literals}.2, otherwise defender removes $(x_2,f)$ or $(l_{j2},x_2)$,
and agents move to $l_{j3}$ and either $h_l$ or $h_r$, and we can apply Lemma~\ref{lem:veri_literals}.3. Thus the ``only-if'' direction of Lemma~\ref{lem:veri} holds.
For the reverse, with the above observation, clearly 
if the defender looses, then $\alpha(G^n_{\psi}) \not \models (L_{j1} \lor L_{j2} \lor L_{j3})$, and thus $\alpha(G^n_{\psi}) \not \models \psi$.

All in all, Lemma~\ref{lem:g_qbf_psi} follows from
Lemmata~\ref{lem:filtering}, \ref{lem:universal}, \ref{lem:existential}, \ref{lem:veri} 
and construction of $\GG^n_{\psi}$.




\section{Blocking problem over trees}\label{sec:tree}

Throughout this section we use the following definitions:
A tree $T$ is a directed acyclic graph such that i) there exists exactly one vertex with indegree $0$ (the root) ii) there exists one vertex with indegree $> 0$ (the goal) and iii) all other vertices have indegree $1$. The depth of a tree is the length of a maximal path, formally $\text{depth}(T) = \max \{ i \in \mathbb{N} \mid V^i \not = \varnothing \}$. where $V^i$ is the set of nodes with a path from the root of length $i$. With $E(i)$ we denote the outgoing
edges w.r.t. to $V^i$, that is $E(i) = \{ (u,v) \in E \mid u \in V^i \}$. The size of a tree $|T|$ is the number of its edges. We say $M$ is a multiset \emph{over} a set $N$ when $N$ is the underlying set of $M$. We speak of decision problems $n$/\textsc{$\infty$-agent blocking} \emph{over trees}, when the input-arena is restricted to a tree. To solve games on trees, we can use a straight-forward attractor construction of the winning-sets of the agents, starting with the most-distant configurations and iteratively consider previously reachable ones. Our result is that as long as we fix the number of the agents and regard it as a constant, the problem becomes polynomially
tractable for arbitrary sized trees, but remains NP-hard, if we allow infinitely many agents.

%FB: I changed the following:
\begin{definition}
Let $\GG = (T, s, f)$ and $d = \text{depth}(T)$. Let $1 \leq i < d$. We define recursively the \emph{winning sets} $W_i$ of the agents. We have $W_d = \{ \{f\}\}$ and 
\begin{align*}
W_{i} = \{ & A \mid \text{$A$ is a multiset over $V^{i}$}, 1 \leq |A| \leq n, \text{and $f \in A$ or}   \\
&	\forall e \in E(i) \,\ \exists B \in W_{i+1}: 
	(E_{\text{in}} \setminus \{e \},A) \toa (E_{\text{in}} \setminus \{ e \},B) \}
\end{align*}
\end{definition}

For the agents, at each step, it is always optimal to move towards the final goal. If some agents are stuck in the tree, due to an outdegree equals to zero, we can considered them lost that means consider only configurations where these agents are removed from $A$. Similarly, the best choice for the defender consists always in deleting one of the edges from $E(i)$ in step $i$.

The set $W_i$ collects exactly all the configurations of agents after $i$ steps, in which the defender cannot prevent them to win; either directly or by reaching a configuration in $W_{i+1}$ despite any removal of an edge. Since agents play first, we only need to compute the set of winning configurations $W_1$; if this set is not empty, the agents move to such a configuration and thus the defender looses.


\begin{lemma}\label{thm:sound_correct}
Let $\GG = (T,s,f)$ be a game arena with root $s$ and goal $f$ and $d = \text{depth}(T)$. The defender wins on $\GG$ against $n$ agents iff $W_1 = \varnothing$.
\end{lemma}

%\begin{lemma}
%Let $\GG = (T,s,f)$ be a game arena with root $s$ and goal $f$.
%\begin{enumerate}
%\item Assume the defender wins against $n$ agents on $\GG$. Then he can do so by only deleting edges from $E(i)$ in step $i$.
%\item Let $(E,A)$ be a configuration. Let $E' \subseteq E$ be the subset of edges, where no adjacent vertex is reachable from any node in $A$, let $A'$ be the set of nodes for which there is no path to the goal, and let $j = \max\{i \mid a \in A \cap V^i\}$. The defender wins in $(E,A)$ iff he wins in $(E \setminus E', A \setminus A')$.
%\end{enumerate}
%\end{lemma}
%FB: I uncommented the next paragraph. Now that we have space, we should briefly explain the lemma.
%FB: Maybe we should also change the text.
%\FB{We should write a more detailled proof here. At least some explanations.}
%We skip the proof for Lemma~\ref{thm:sound_correct}, but mention that the key point is here that whenever the defender has a winning strategy, he has one where he deletes in step $i$ an edge from $\{ (v,u) \mid v \in V^i \}$. Thereby the number of all branchings that need to be considered is reduced significantly.

\begin{theorem}
Let $(T,s,f)$ be a game arena over a tree $T$ with root $s$, where
$n$ agents placed at $s$. Then $W_0$ can be 
computed in time $O(|T|^{2n+2})$. %DK changed bound here
\end{theorem}
\begin{proof}
We only give a brief sketch:
The size of $W_i$ can be (over)estimated in the following way:
Since the size of each multiset in $W_i$ is limited by $n$, 
and there are $|V^i|$ choices for each element, we
have $W_i \leq |V^i|^n \leq |T|^n$. We can first generate the set
of all potential elements of $W_i$, and then filter out those
that do not adhere the conditions. The first condition can
be checked during the construction, and to check the second
condition for $W_i$, we need to remove each of $|E(i)|$ edges, 
and then,
for each of this removal test all potential moves of the agents.
Each of the $n$ many agents at, say $u$, has at most 
$\textsf{outdeg}(u)$ choices to move. Thus there are
at most $|\sum_{u \in V^i} \textsf{outdeg}(u)|^n \leq |T|^n$
moves that have to be tested $|E(i)|$ times. Then one $W_i$ can
be computed in  %\in O(|T|^n)
\[
O(|T|^n \cdot |E(i)| \cdot |T|^n) = O(|T|^{2n+1}) 
\] and since there are at most $\text{depth}(T) \leq |T|$ sets $W_i$
to generate, $W_0$ can be computed in $|T| \cdot O(|T|^n) = O(|T|^{2n+2})$.
\end{proof}

\begin{corollary}
For a fixed number of agents, \textsc{$n$-agent blocking} over trees is 
decidable in polynomial time in the size of the tree.
\end{corollary}

\noindent For infinitely man agents however, NP-hardness remains. In \cite{KG10}, the following variant of the Firefighter-problem is introduced and shown to be NP-hard:
\begin{quote}
\textsc{3-fl-fire} is the following decision problem: \\
\textsf{Input:} A full rooted~\footnote{A tree is full rooted, if all leaves have the same distance from the root} tree $T$ with maximum degree $3$ and root $r$. \\
\textsf{Question:} Is there a sequence of vertex deletions, such that no leaf burns?
\end{quote}

\noindent In \textsc{3-fl-fire}, in the first step a fire breaks out at the root. In each subsequent
step, the firefighter defends a vertex which is not on fire (the vertex stays protected afterwards), and then, when a vertex 
is burning, the fire spreads to all children of the vertex. This continues, until
the fire cannot spread anymore.
Thus the main difference between \textsc{3-fl-fire} and \textsc{$\infty$-agent blocking} over trees is merely edge-deletions vs. vertex deletions. A reduction is straight-forward:

\begin{theorem}\label{thm:tree_np}
\textsc{$\infty$-agent blocking} over trees is NP-hard.
\end{theorem}
\begin{proof}
First note that if the (infinitely many) agents win on a tree, they always win by pursuing all outgoing links in any configuration, thus acting like the fire. We use this fact in the reduction:
Given an instance of \textsc{3-fl-fire} and tree $T$ and root $r$, construct the following arena $(T',r,f)$: (i) Add a designated goal node $f$ (ii) add an edge $(l,f)$ for each leaf $l$ (iii) add a path of length $\text{depth}+1$ from $r$ to $f$. Assume the firefighters win on $T$ by removing $v_1, v_2, \ldots v_n$. Let $(u',f)$ be on the path constructed in (iii). Then the defender wins on $T'$ by deleting $(u,v_1)$, $(u,v_2)$ ... $(u,v_n)$ and finally $(u',f)$. On the other hand, if the firefighters loose on $T$, then there is at least one fire at a leaf. Thus there are agents at at least one leaf, and agents at $u'$ and the defender looses.
\end{proof}


\section{Conclusion}\label{sec:Conclusion}

We considered the multi-agent sabotage game over directed acyclic graphs, where multiple agents move along edges while the graph is subject to edge deletions by a defender. We established PSPACE-completeness of the \textsc{$n$-agent blocking} problem for $n\geq 2$ and NP-completeness of the \textsc{$\infty$-agent blocking} problem, where the game is played with respectively, a finite number $n$ of agents, and an infinite number of agents. This extends the result on PSPACE-completeness of Sabotage Games in that when considering the reachability problem in a crumbling network, adding a notion of distributivity yields a similar shift in complexity as adding the ability to have multi-edges.

To conclude the paper, we give the following open problems:
\begin{itemize}
\item 
Considering large graphs or networks, deciding the problem in practice is a huge challenge. This is not only due to the theoretical result of PSPACE-hardness shown here, but also due to the huge branching factor induced by the large number of possible moves of agents in each step. While much progress has been made on solving PSPACE-complete problems in practice by dedicated \textsc{qbf}- and \textsc{qcsp}-solver, an encoding into \textsc{qbf} or \textsc{qcsp} is impractical, and it is a challenge to transfer such algorithmic improvements to our setting.
\item
In this paper, agents are globally controlled by an external observer who plays the game with perfect information. Considering a more realistic model where agents have partial vision or limited communication capabilities, for example restricted to other agents located on the same node; there exist game arenas where they are not able to compute a winning strategy in a distributed manner, even if such a strategy exists. Therefore it remains a challenge to define distributed algorithms solving the multiple-agent sabotage game.
\end{itemize}

\subsubsection*{Acknowledgements}

We thank Nao Hirokawa for his valuable comments on an earlier draft, and we 
thank Shuji Kijima for pointing us to the Firefighter-problem.

\selectlanguage{english}
\bibliography{references}

\setcounter{page}{1}
\pagenumbering{roman}

\appendix
\section{Games with infinitely many agents}\label{sec:app-infty}

One might ask, what happens if there is a infinite supply of 
agents to ``flood'' a network.  Then there are always 
enough agents to move alongside any outgoing edge in any 
configuration. 

%DK changed notion of configuration according to new definition, f -> \sigma
Given an arena $(G,s,f)$, the initial configuration of a 
game with infinitely many agents
is $(E_{\text{in}},A_{\text{in}})$, where 
$A_{\text{in}}$ is a multiset containing the element $s$
with cardinality $\mathbb{N}$. Let $C$ be the set of 
configurations.
A strategy of the agents is a function $\sigma: C \to C$ with
$c \toa \sigma(c)$ for all $c \in C$. Let $(E,A) \toa (E',A')$ 
be a move of the agents with multisets $S$ and $M$ as defined.
A move is \emph{all-exploring} if 
$\{ s \mid s \in A, (s,t) \in E \} \setminus M_s = \varnothing$.
Here the set $M_s$ denotes the underlying set of elements of $M$.
A strategy $\sigma$ is \emph{all-exploring} 
if for all $c \in C$, the move $c \toa \sigma(c)$ is all-exploring.
The agents play according to a strategy $\sigma$, if whenever
being in configuration $c$, agents move $c \toa \sigma(c)$.

\begin{description}
\item
\textsc{$\infty$-agent blocking}:\\
\textsf{Input:} A game arena $\GG$. \\
\textsf{Question:} Does the defender win in $\GG$ against infinitely many agents?
\end{description}

An all-exploring strategy is always optimal for the agents.
Note we implicitly already used the next Lemma in the proof of 
Theorem~\ref{thm:tree_np}:

\begin{lemma}
Let $\GG$ be a game arena. Fix any all-exploring strategy $\sigma$,
the defender wins in $\GG$ against infinitely-many agents 
iff he wins against infinitely-many agents playing according to $\sigma$.
\end{lemma}

Thus to decide the blocking problem against infinitely many agents,
it suffices to only consider one unique move of the agents in
a configuration. However this does not shift the problem to $P$:

\begin{theorem}\label{thm:np-complete}
\textsc{$\infty$-agent blocking} is NP-complete.
\end{theorem}

Here we only show NP-hardness. For it,
we give a reduction 
from the NP-complete problem \textsc{sat}~\cite{CO71}.
Let $\varphi$ be a quantifier free formula over $m$ Boolean variables 
$X_1, \ldots X_m$ in conjunctive normal form. Then 
$\psi = \exists X_1 \ldots \exists X_m \varphi$ is an instance of \textsc{sat}.
Note that w.l.o.g. we can require each clause to contain exactly three variables.
Analogous to the reduction from \textsc{qbf}, we will construct a game arena
$\GG_{\psi}$ polynomial in the size of the formula, where
the defender wins against infinitely many agents
iff the instance of \textsc{sat} has a satisfying assignment.

\begin{lemma}\label{lem:g_sat_psi}
Let $\psi$ be an instance of \textsc{sat}.
The defender wins on $\GG_{\psi}$
iff $\psi$ has a satisfying assignment.
\end{lemma}

Lemma~\ref{lem:g_sat_psi} and polynomial size of the game 
arena in the size of $\psi$, proves 
Theorem~\ref{thm:np-complete}. We 
construct existential gadgets for each variable and a verification gadget.
The gadgets however are different here, since, in contrast to the previous 
reduction, the adversary now needs to verify his assignment 
on \emph{all} clauses. For $\GG_{\psi} =(G,s,f)$ we set $s$
as node $s_1$ of the first existential gadget. The exit $s_2$
of the existential gadget of $X_1$ is the entry $s_2$ of the existential
gadget for $X_2$ and so on, until the exit $s_{m+1}$ of the existential
gadget for $X_m$ is the entry $c_1$ of the verification gadget.
The literal nodes $l_{jk}$ of the verification-gadget and variable nodes $x_i$
are connected in the following way: Let $L_{jk}$
denote the $k$-th literal of clause $j$ of $\psi$. Then
$(l_{jk},x_i) \in E$ iff $L_{jk} = x_i$, and 
$(l_{jk},\neg x_i) \in E$ iff $L_{jk} = \neg x_i$.
The existential gadget is shown in Figure~\ref{fig:existential-gadget-inf},
and the verification gadget is shown in Figure~\ref{fig:verification-gadget-inf}.


\begin{figure}[t]%
  \centering
  % The existential gadget for infintiely many attackers
  \begin{tikzpicture}[scale=0.2,node distance=1cm,style=mystyle]
   \tikzstyle{every to}=[->] %make all edges directed

 	\node[]								(fake_in)	at (0,0)			{};
 	\node[]								(a)			[right of=fake_in]  {$s_i$};
    \node[node distance=0.8cm]			(b)			[below of=a] {$a$};    
   
    \node[node distance=2.41cm, style=final](f) 	[below of=b]		{$\bullet$};    
    \node[node distance=2cm]			(bl)		[below left of=b]	{$b_l$};
    \node[node distance = 2cm]			(br)		[below right of=b]	{$b_r$};   

    \node[]								(cl)		[below of=bl]		{$c_l$};   
    \node[]								(cr)		[below of=br]		{$c_r$};   
    \node[]								(el)		[below of=cl]		{$x_i$};   
    \node[]								(er)		[below of=cr]		{$\neg x_i$};   
    \node[]								(dl)		[left of=el]		{$d_l$};   
    \node[]								(dr)		[right of=er]		{$d_r$};   
    \node[node distance=2cm]			(g)			[below of=f]		{$s_{i+1}$};
    \node[]								(o)			[below of=g]		{};

    
    \node[node distance=2cm]			(h)			[left of=cl]		{$h$};    
    \node[]								(i)			[below of=h]		{$i$};
    \node[style=final]					(f2)		[left of=i]			{$\bullet$};
    \node[]								(k)			[below of=i]		{$k$};
    \node[]								(j)			[below of=f2]		{$j$};

    \node[node distance=3cm]		(from_veri1)[above left of=i]	{\tiny{ver. gadget}};
    \node[node distance=1.5cm]		(from_veri2)[above right of=dr]	{\tiny{ver. gadget}};
 
	\draw[]							(b)		to node[auto]	{}	(bl); 
	\draw[]							(b)		to node[auto]	{}	(br);     
	\draw[]							(bl)	to node[auto]	{}	(cl); 	
	\draw[]							(br)	to node[auto]	{}	(cr); 		
	\draw[]							(cl)	to node[auto]	{}	(dl); 		
	\draw[]							(cr)	to node[auto]	{}	(dr); 		
	\draw[]							(dl)	to node[auto]	{}	(g); 	
	\draw[]							(dr)	to node[auto]	{}	(g); 	
	\draw[]							(dl)	to node[auto]	{}	(el); 	
	\draw[]							(dr)	to node[auto]	{}	(er); 			
		
	\draw[]							(h)		to node[auto]	{}	(i); 	
	

	\draw[]							(k)		to node[auto]	{}	(g); 	
	\draw[]							(i)		to node[auto]	{}	(k); 	
	\draw[]							(k)		to node[auto]	{}	(j); 	
	\draw[]							(j)		to node[auto]	{}	(f2); 	
	
	\draw[]							(cl)	to node[auto]	{}	(f); 	
	\draw[]							(bl)	to node[auto]	{}	(f); 	
	\draw[]							(cr)	to node[auto]	{}	(f); 	
	\draw[]							(br)	to node[auto]	{}	(f); 	
	\draw[]							(el)	to node[auto]	{}	(f); 	
	\draw[]							(er)	to node[auto]	{}	(f); 	

	

	\draw[]							(a)		to node[auto]	{}	(b);
%    \draw[style=ledge,dotted]	(fake_in)	to node[auto]	{in}    (a);   
%    \draw[style=ledge,dotted]	(g)			to node[auto]	{out}	(o);

	\draw[bend left=30,style=ledge,dotted]	(from_veri1) to node[auto] {} (el);
	\draw[bend right=20,style=ledge,dotted]	(from_veri2) to node[auto] {} (er);
	\draw[bend right=10]		(b)	to node[auto]	{}	(h);

	
  \end{tikzpicture}
  \caption{The initial {\emph existential}-gadget for variable $X_i$.}
  \label{fig:existential-gadget-inf}
\end{figure}




\begin{figure}[hbt]%
  \centering
  % The verification gadget, infinitely many attackers
  \begin{tikzpicture}[scale=0.5,node distance=1cm,style=mystyle]
   \tikzstyle{every to}=[->] %make all edges directed

 	\node[]								(fake_in)	at (0,0)			{$s_{m+1}$};
 	\node[]								(c1)		[below of=fake_in]  {$c_1$};
 	\node[node distance=2cm]			(c2)		[right of=c1] 		{$c_2$};
 	\node[node distance=4.5cm]			(ck)		[right of=c2]		{$c_p$};
 	
 	\node[node distance=2cm]			(fake_belowc2)[below of=c2]		{};
 	\node[node distance=4cm]			(fake_belowc21)[below of=c2]	{};
 	\node[node distance=1.5cm]			(fake_rightc2)[right of=c2]		{};
 	\node[node distance=3cm]			(fake_rightc21)[right of=c2]	{};
 	
 	\node[]								(abovec2)	[above of=c2]		{$e_1$};
 	\node[]								(aboveck)	[above of=ck]		{$e_{p-1}$};
 	
 	\node[node distance=1.8cm]			(fake_in_ck1)	[left of=aboveck] {};
 	\node[node distance=2.3cm]			(fake_in_ck2)	[left of=aboveck] {};
 	\node[node distance=2.8cm]			(fake_in_ck3)	[left of=aboveck] {};

 	\node[]								(b1)		[below of=c1]		{$b_{11}$};
 	\node[]								(l11)		[left of=b1]		{$l_{11}$};
 	\node[]								(fake_l11l)	[left of=l11]		{$d_{11}$};
 	\node[style=final]					(f1)		[left of=fake_l11l]	{$\bullet$};
	\node[]								(back11)	[below of=fake_l11l]{};
	\node[style=final]					(f2)		[right of=b1]		{$\bullet$};
	\node[]								(b2)		[below of=b1]		{$b_{12}$};
	\node[style=final]					(f3)		[right of=b2]		{$\bullet$};
	\node[]								(b3)		[below of=b2]		{$b_{13}$};
	\node[]								(b4)		[below of=b3]		{$b_{14}$};
	\node[]								(l12)		[left of=b4]	{$l_{12}$};
	\node[]								(fake_l12l)	[left of=l12]		{$d_{12}$};
	\node[style=final]					(f4)		[left of=fake_l12l]	{$\bullet$};
	\node[]								(back12)	[below of=fake_l12l]{};
	\node[style=final]					(f5)		[right of=b4]		{$\bullet$};
	\node[]								(b5)		[below of=b4]		{$b_{15}$};
	\node[style=final]					(f6)		[right of=b5]		{$\bullet$};
	\node[]								(fake_l13)	[below of=b5]		{};
	\node[]								(l13)		[left of=fake_l13]	{$l_{13}$};
	\node[]								(fake_l13l)	[left of=l13]		{$d_{13}$};			
	\node[style=final]					(f7)		[left of=fake_l13l] {$\bullet$};
	\node[]								(fake_l14)	[below of=l13]		{};
	\node[]								(back13)	[left of=fake_l14]	{};
		
	\draw[]							(c1)	to node[auto]	{}	(l11); 	
	\draw[]							(c1)	to node[auto]	{}	(b1); 	
	\draw[]							(l11)	to node[auto]	{}	(fake_l11l); 		
	\draw[]							(fake_l11l)	to node[auto]	{}	(f1); 	
	\draw[]							(b1)	to node[auto]	{}	(b2); 		
	\draw[]							(b1)	to node[auto]	{}	(f2); 		
	\draw[]							(b2)	to node[auto]	{}	(f3); 	
	\draw[]							(b2)	to node[auto]	{}	(b3); 		
	\draw[]							(b3)	to node[auto]	{}	(l12); 	
	\draw[]							(b3)	to node[auto]	{}	(b4); 		
	\draw[]							(b4)	to node[auto]	{}	(b5); 		
	\draw[]							(b4)	to node[auto]	{}	(f5); 		
	\draw[]							(b5)	to node[auto]	{}	(f6); 		
	\draw[]							(l12)	to node[auto]	{}  (fake_l12l);
	\draw[]							(fake_l12l)	to node[auto]	{}  (f4);	
	\draw[]							(b5)	to node[auto]	{}  (l13);	
	\draw[]							(l13)	to node[auto]	{}  (fake_l13l);	
	\draw[]							(fake_l13l)	to node[auto]	{}  (f7);	
	
	\draw[bend right =40]			(l11)	to node[auto]	{}  (f1);	
	\draw[bend right =40]			(l12)	to node[auto]	{}  (f4);	
	\draw[bend right =40]			(l13)	to node[auto]	{}  (f7);		
	
	\draw[style=ledge,dotted]		(l11)		to node[auto]	{\tiny{back}}	(back11);		
	\draw[style=ledge,dotted]		(l12)		to node[auto]	{\tiny{back}}	(back12);	
	\draw[style=ledge,dotted]		(l13)		to node[auto]	{\tiny{back}}	(back13);	
	

 	\node[]								(bk1)		[below of=ck]		{$b_{p1}$};
 	\node[]								(lk1)		[left of=bk1]		{$l_{p1}$};
 	\node[]								(fake_lk1l)	[left of= lk1]		{$d_{p1}$};
 	\node[style=final]					(fk1)		[left of=fake_lk1l]	{$\bullet$};
	\node[]								(backk1)	[below of=fake_lk1l]{};
	\node[style=final]					(fk2)		[right of=bk1]		{$\bullet$};
	\node[]								(bk2)		[below of=bk1]		{$b_{p2}$};
	\node[style=final]					(fk3)		[right of=bk2]		{$\bullet$};
	\node[]								(bk3)		[below of=bk2]		{$b_{p3}$};
	\node[]								(bk4)		[below of=bk3]		{$b_{p4}$};	
	\node[]								(lk2)		[left of=bk4]		{$l_{p2}$};
	\node[]								(fake_lk2l)	[left of=lk2]		{$d_{p2}$};
	\node[style=final]					(fk4)		[left of=fake_lk2l]	{$\bullet$};
	\node[]								(backk2)	[below of=fake_lk2l]{};
	\node[style=final]					(fk5)		[right of=bk4]		{$\bullet$};
	\node[]								(bk5)		[below of=bk4]		{$b_{p5}$};
	\node[style=final]					(fk6)		[right of=bk5]		{$\bullet$};
	\node[]								(fake_lk3)	[below of=bk5]		{};
	\node[]								(lk3)		[left of=fake_lk3]	{$l_{p3}$};
	\node[]								(fake_lk3l)	[left of=lk3]		{$d_{p3}$};			
	\node[style=final]					(fk7)		[left of=fake_lk3l] {$\bullet$};
	\node[]								(fake_lk4)	[below of=lk3]		{};
	\node[]								(backk3)	[left of=fake_lk4]	{};
		
	\draw[]							(ck)	to node[auto]	{}	(lk1); 	
	\draw[]							(ck)	to node[auto]	{}	(bk1); 	
	\draw[]							(lk1)	to node[auto]	{}	(fake_lk1l); 		
	\draw[]							(fake_lk1l)	to node[auto]	{}	(fk1); 	
	\draw[]							(bk1)	to node[auto]	{}	(bk2); 		
	\draw[]							(bk1)	to node[auto]	{}	(fk2); 		
	\draw[]							(bk2)	to node[auto]	{}	(fk3); 	
	\draw[]							(bk2)	to node[auto]	{}	(bk3); 		
	\draw[]							(bk3)	to node[auto]	{}	(lk2); 	
	\draw[]							(bk3)	to node[auto]	{}	(bk4); 		
	\draw[]							(bk4)	to node[auto]	{}	(bk5); 		
	\draw[]							(bk4)	to node[auto]	{}	(fk5); 		
	\draw[]							(bk5)	to node[auto]	{}	(fk6); 		
	\draw[]							(lk2)	to node[auto]	{}  (fake_lk2l);
	\draw[]							(fake_lk2l)	to node[auto]	{}  (fk4);	
	\draw[]							(bk5)	to node[auto]	{}  (lk3);	
	\draw[]							(lk3)	to node[auto]	{}  (fake_lk3l);	
	\draw[]							(fake_lk3l)	to node[auto]	{}  (fk7);	
	
	\draw[bend right =40]			(lk1)	to node[auto]	{}  (fk1);	
	\draw[bend right =40]			(lk2)	to node[auto]	{}  (fk4);	
	\draw[bend right =40]			(lk3)	to node[auto]	{}  (fk7);		
	
	\draw[style=ledge,dotted]		(lk1)		to node[auto]	{\tiny{back}}	(backk1);		
	\draw[style=ledge,dotted]		(lk2)		to node[auto]	{\tiny{back}}	(backk2);	
	\draw[style=ledge,dotted]		(lk3)		to node[auto]	{\tiny{back}}	(backk3);	

 	\draw[style=dotted] (fake_belowc2) 	to[-] node[auto] {} (fake_belowc21);
 	\draw[style=dotted] (fake_rightc2) 	to[-] node[auto] {} (fake_rightc21);

	\draw[]							(abovec2)	to node[auto]	{}	(c2);
	\draw[]							(aboveck)	to node[auto]	{}	(ck);
	
	\draw[bend left=90,looseness=1.2]		(l11)		to node[auto]		{} (abovec2);
	\draw[bend left=30]		(l12)		to node[auto]		{} (abovec2);
	\draw[bend right=40]	(l13)		to node[auto]		{} (abovec2);

	\draw[bend left=10]		(fake_in_ck1)		to node[auto]		{} (aboveck);
	\draw[bend left=20]		(fake_in_ck2)		to node[auto]		{} (aboveck);
	\draw[bend left=30]		(fake_in_ck3)		to node[auto]		{} (aboveck);

    \draw[]	(fake_in)	to node[auto]	{}    (c1);  

  \end{tikzpicture}
  \caption{Verification-gadget, infinitely many agents, $p$ clauses.}
  \label{fig:verification-gadget-inf}
\end{figure}


We give a description on how to construct $\GG_{\psi}$ of Lemma~\ref{lem:g_sat_psi}.
The definition of an assignment of a variable \emph{in} $\GG_{\psi}$ is analogous as for the proof of PSPACE-hardness:

\begin{definition}
Let $\GG_{\psi} = (G,s,f)$ be the game arena for a given instance $\psi$ of \textsc{sat}, and $(E,A)$ a configuration. Variable
$X_i$ is assigned \emph{in} $\GG_{\psi}$ to
\begin{align*}
&\text{\textsc{false}, when $(x_i,f) \in E$ and $\textsf{outdeg}(\neg x_i) = 0$}  \\
&\text{\textsc{true}, when $(\neg x_i,f) \in E$ and $\textsf{outdeg}(x_i) = 0$}  
\end{align*}
We write $\GG_{\psi}(X_i) = \textsc{true}$ resp. $\GG_{\psi}(X_i) = \textsc{false}$,
and we write $\alpha(\GG_{\psi})$ to denote 
the assignment of the variables of $\psi$ where $X_i = \textsc{true}$ when 
$\GG_{\psi}(X_i) = \textsc{true}$ and $X_i = \textsc{false}$ when $\GG_{\psi}(X_i) = \textsc{false}$.
\end{definition}

\subsection*{Existential-gadget for infinitely many agents}

The existential gadget is a slight variation of the one for $n$ agents.
Again, the defender has the choice of assigning variable $X_i$ \emph{in}
$G_{\psi}$.

\begin{lemma}\label{lem:existential}
Let $X_i$ be the variable of an existential-gadget of $\GG_{\psi}$, and $(E,\{s_i, s_i\})$ be a configuration, where the edges of the gadget $E_e \subseteq E$ are the intact.
Let both player play optimally.
Then a traversal of the existential-gadget leads to a configuration $(E',\{s_{i+1}, s_{i+1}\})$ 
where $E' \setminus E_e = E \setminus E_e$ and, \emph{depending on the deletions of the defender}, either
$\GG_{\psi}(X_i) = \textsc{true}$ or $\GG_{\psi}(X_i) = \textsc{false}$.
\end{lemma}

A traversal starts with the agents moving to $a$. Then the defender has to remove
either $(a,b_l)$ or $(a,b_r)$: Assume he removes any edge except $(b_l,f)$ or $(b_r,f)$.
Then the agents win by moving in parallel $b_l$ and $b_r$, and in the next step to $f$.
If the defender removed $(b_l,f)$ ($(b_r,f)$), then the agents win by moving to 
$b_l$ and $b_r$, the agent has to remove $(b_r,f)$ ($(b_l,f)$), agents move to $c_l$
and $c_r$ and win in the next step.

Assume w.l.o.g. the defender removed $(b_l,f)$ in the first step, thereby yielding
the change to set later $\GG_{\psi}(X_i)=\textsc{false}$. 
Agents move to $b_l$ and $h$, defender removes
$(b_l,f)$, agents move to $i$ and $c_l$, defender removes $(c_l,f)$ and the agents
move to $k$ and $d_l$. Now the agent has to remove either $(d_l,x_i)$, $(x_i,f)$,
$(k,j)$ or $(j,f)$, otherwise agent win by moving to $j$ and $x_i$. We make a case 
distinction:
\begin{itemize}
\item Defender removes $(x_i,f)$. Agents move to $j$ and $s_{i+1}$, agent removes
$(j,f)$ and the game is in a configuration, as described in Lemma~\ref{lem:existential}.
\item Defender removes $(k,j)$ or $(j,f)$. Agents move to $s_{i+1}$ and $x_i$,
agent removes $(x_i,f)$ and again we are in a configuration with the properties
as described in Lemma~\ref{lem:existential}.
\item Defender removes $(d_l,x_i)$. Agents move to $j$ and $s_{i+1}$, defender
removes $(j,f)$. Now $X_i$ is neither assigned to \textsc{true} nor to \textsc{false} 
in $\GG_{\psi}$ and this not optimal for the defender, since it will affect
his ability to win in the verification-gadget.
\end{itemize}

In all cases, when playing optimally, the defender reaches a configuration with
the properties as described in Lemma~\ref{lem:existential}.

\subsection*{Verification-gadget for infinitely many agents}

As in the proof for $n$ agents, there is a direct correspondence between
literal nodes $l_{jk}$ and the assignment of the variables:

\begin{lemma}\label{lem:veri_literalsBIS} %FB: The same label was used twice.
Let $\GG_{\psi}$ be the game arena of $\psi$, and $(E,A)$ a configuration,
where all variables of $\psi = C_1 \land \cdots \land C_p$ 
are assigned \emph{in} $\GG_{\psi}$, and
defender is about to move. Assume infinitely many agents are at $c_1$.
Then the defender wins iff $\alpha(\GG_{\psi}) \models \psi$.
\end{lemma}

We only give an informal description of the traversals:
Assume $\alpha(\GG_{\psi}) \models \psi$. Then 
$\alpha(\GG_{\psi} \models (L_{11} \lor L_{12} \lor L_{13})$. 
The traversal starts with agents at $c_1$ and the defenders
turn. He has to remove $(c_1,l_{11})$ or $(c_1,b_{11})$, otherwise the agents
win by moving to both $l_{11}$ and $b_{11}$. If both $(l_{11},f)$ and $(b_{11},f)$
are intact, they win by moving on one of the edges to $f$. If only one edge is 
intact, the defender has to remove it, and then agents move to $d_{11}$ and $b_{12}$
and win in the next step.
W.l.o.g. let $L_{11} = X_i$. When $\alpha(\GG_{\psi}) \models L_{11}$, 
then $(x_i,f) \not \in E$, i.e. $x_i$ is a sink.
Thus the defender removes $(c_1,b_{11})$, agents move to $l_{11}$, defender 
removes $(l_{11},f)$ and the agents move to $d_{11}$, $x_i$ and $e_1$.
They are stuck in $x_i$, thus the agent removes $(d_{11},f)$ and agents move
to $c_2$ and the verification for the next clause starts.

Otherwise, when $\alpha(\GG_{\psi}) \not \models L_{11}$, defender 
removes $(c_1,l_{11})$. After two steps and removals of $(b_{11},f)$ and
$(b_{12},f)$, agents reach $b_{13}$. When 
$\alpha(\GG_{\psi}) \models L_{12}$, defender removes $(b_{13},b_{14})$ and
the verification for the next clause starts, similar to the 
previous case when $\alpha(\GG_{\psi}) \models L_{11}$.
Otherwise she removes $(b_{13},l_{12})$, and after two steps, agents will
reach $l_{13}$. When $\alpha(\GG_{\psi}) \models L_{13}$, then defender
removes $(l_{13},f)$ and then $(d_{13},f)$, and the verification 
for the next clause starts. When $\alpha(\GG_{\psi}) \not \models L_{13}$, 
the defender looses: 
Let $L_{13} = X_i$. After removing $(l_{13},f)$, agents move to both
$d_{13}$ and $x_i$, and due to $\alpha(\GG_{\psi}) \not \models L_{13}$,
edge $(x_i,f) \in E$ and the defender looses. But that only means that
defender looses when $\alpha(\GG_{\psi}) \not \models L_{13} \lor L_{12} \lor L_{13}$, i.e. 
$\alpha(\GG_{\psi}) \not \models \psi$.
Note that for the verification of the last clause (i.e. below $c_p$), 
there are only three outgoing edges from $l_{pk}$, i.e. the traversal stops there.




\end{document}